(module inferrer  (lib "eopl.ss" "eopl")
  
  (require "drscheme-init.scm")
  (require "lang.scm")
  (require "data-structures.scm")
  (require "unifier.scm")
  
  (provide type-of-program type-of)
  
  ;;;;;;;;;;;;;;;; The Type Checker ;;;;;;;;;;;;;;;;
  
  ;; we'll be thinking of the type of an expression as pair consisting
  ;; of a type (possibly with some type variables in it) and a
  ;; substitution that tells us how to interpret those type variables.
  
  ;; answer = type * subst
  ;; type-of: exp * tenv * subst  -> answer
  
  ;; we may change this once we get it working.
  
  (define-datatype answer answer?
    (an-answer
     (type type?)
     (subst substitution?)))
  
  (define type-of-program
    (lambda (pgm)
      (cases program pgm
        (a-program (exp1)
                   (cases answer (type-of exp1 (init-tenv) (empty-subst))
                     (an-answer (ty subst)
                                (apply-subst-to-type ty subst)))))))
  
  (define type-of
    (lambda (exp tenv subst)
      (cases expression exp
        
        (const-exp (num) (an-answer (int-type) subst))
        
        (zero?-exp (exp1)
                   (cases answer (type-of exp1 tenv subst)
                     (an-answer (type1 subst1)
                                (let ((subst2 (unifier type1 (int-type) subst1 exp)))
                                  (an-answer (bool-type) subst2)))))
        
        (diff-exp (exp1 exp2)
                  (cases answer (type-of exp1 tenv subst)
                    (an-answer (type1 subst1)
                               (let ((subst1 (unifier type1 (int-type) subst1 exp1)))
                                 (cases answer (type-of exp2 tenv subst1)
                                   (an-answer (type2 subst2)
                                              (let ((subst2
                                                     (unifier type2 (int-type) subst2 exp2)))
                                                (an-answer (int-type) subst2))))))))
        
        (if-exp (exp1 exp2 exp3)
                (cases answer (type-of exp1 tenv subst)
                  (an-answer (ty1 subst)
                             (let ((subst (unifier ty1 (bool-type) subst exp1)))
                               (cases answer (type-of exp2 tenv subst)
                                 (an-answer (ty2 subst)
                                            (cases answer (type-of exp3 tenv subst)
                                              (an-answer (ty3 subst)
                                                         (let ((subst (unifier ty2 ty3 subst exp)))
                                                           (an-answer ty2 subst))))))))))
        
        (null-exp (exp)
                  (cases answer (type-of exp tenv subst)
                    (an-answer (typ subst)
                               (an-answer (bool-type) subst)
                               )))
        
        (var-exp (var) (an-answer (apply-tenv tenv var) subst))
        
        (let-exp (var exp1 body)
                 (cases answer (type-of exp1 tenv subst)
                   (an-answer (rhs-type subst)
                              (type-of body
                                       (extend-tenv var rhs-type tenv)
                                       subst))))
        
        (proc-exp (var otype body)
                  (let ((arg-type (otype->type otype)))
                    (cases answer (type-of body
                                           (extend-tenv var arg-type tenv)
                                           subst)
                      (an-answer (result-type subst)
                                 (an-answer
                                  (proc-type arg-type result-type)
                                  subst)))))
        
        (call-exp (rator rand)
                  (let ((result-type (fresh-tvar-type)))
                    (cases answer (type-of rator tenv subst)
                      (an-answer (rator-type subst)
                                 (cases answer (type-of rand tenv subst)
                                   (an-answer (rand-type subst)
                                              (let ((subst
                                                     (unifier rator-type
                                                              (proc-type rand-type result-type)
                                                              subst
                                                              exp)))
                                                (an-answer result-type subst))))))))
        
        (letrec-exp (proc-result-otype proc-name 
                                       bvar proc-arg-otype 
                                       proc-body
                                       letrec-body)
                    (let ((proc-result-type
                           (otype->type proc-result-otype)) 
                          (proc-arg-type
                           (otype->type proc-arg-otype)))
                      (let ((tenv-for-letrec-body
                             (extend-tenv proc-name
                                          (proc-type proc-arg-type proc-result-type) tenv)))
                        (cases answer (type-of proc-body (extend-tenv
                                                          bvar proc-arg-type tenv-for-letrec-body) subst)
                          (an-answer (proc-body-type subst)
                                     (let ((subst (unifier proc-body-type proc-result-type subst proc-body))) 
                                       (type-of letrec-body
                                                tenv-for-letrec-body subst)))))))
        
        (list-exp (e es);;works
                  (letrec
                      ((type-of-list-exps
                        (lambda (e es)
                          (cases answer (type-of e tenv subst)
                            (an-answer (type1 subst)
                                       (if (null? es)
                                           (an-answer (list-type type1) subst);;;;;;;;problem here
                                           (cases answer (type-of (car es) tenv subst)
                                             (an-answer (type2 subst)
                                                        (if (equal? type1 type2)
                                                            (let ((subst (unifier type1 type2 subst e)))
                                                              (type-of-list-exps (car es) (cdr es)))
                                                            (eopl:error 'type-of-list-exp  
                                                                        "Types didn't match: ~s != ~a"
                                                                        (type-to-external-form type1)
                                                                        (type-to-external-form type2)
                                                                        ))))))))))
                    (type-of-list-exps e es)))
        
        (cons-exp (e1 e2);;works
                  (cases answer (type-of e1 tenv subst)
                    (an-answer (type1 subst)
                               (cases answer (type-of e2 tenv subst)
                                 (an-answer (type2 subst)
                                            (let ((subst (unifier type1 type2 subst e1)))
                                              (an-answer (list-type type1) subst)))))))
        
        (car-exp (expressions);;works
                 (type-of (car expressions) tenv subst))
        
        (cdr-exp (expressions);;works
                 (type-of (list-exp (car expressions) (cdr expressions)) tenv subst))
        
        (emptylist-exp ();;is it correct???
                       (an-answer (tvar-type 3) subst))
        
         ;;Explicit-refs
        
        (newref-exp (exp)
                    (cases answer (type-of exp tenv subst)
                      (an-answer (rtype subst)
                                 (an-answer (refto-type rtype) subst))))
        (deref-exp (rexp)
                   (cases answer (type-of rexp tenv subst)
                     (an-answer (rtype subst)
                                (cases type rtype
                                  (refto-type (ty)
                                              (an-answer ty subst))
                                  (else (eopl:error 'type-of-list-exp  
                                                    "Not a Ref-type "
                                                    )
                                        )
                                  ))))
        (setref-exp (e1 e2)
                    (cases answer (type-of e1 tenv subst)
                      (an-answer (rtype subst)
                                 (cases type rtype
                                   (refto-type (ty1)
                                               (cases answer 
                                                 (type-of e2 tenv subst)
                                                 (an-answer (ty2 subst)
                                                            (if (equal? ty1 ty2)
                                                                (let ((subst1
                                                                       (unifier ty1
                                                                                ty2
                                                                                subst
                                                                                exp)))
                                                                  (an-answer
                                                                   (void-type)subst1))
                                                                (eopl:error 'type-of-list-exp  
                                                                            "Types didn't match: ~s != ~a"
                                                                            (type-to-external-form ty1)
                                                                            (type-to-external-form ty2)
                                                                            )))))
                                   (else (eopl:error 'type-of-list-exp  
                                                     "Not a REF-type"
                                                     ))
                                   ))))
        (begin-exp (e1 es)
                   (letrec
                       ((type-of-begin
                         (lambda (exp1 exps)
                           (cases answer (type-of exp tenv exp)
                             (an-answer (ty1 subst)
                                        (if (null? exps)
                                            (an-answer ty1 subst)
                                            (type-of-begin (car exps) (cdr exps))
                                            ))))))
                     (type-of-begin e1 es)))
       
        ) ))
  
  ;;;;;;;;;;;;;;;; type environments ;;;;;;;;;;;;;;;;
  
  ;; why are these separated?()
  
  (define-datatype type-environment type-environment?
    (empty-tenv-record)
    (extended-tenv-record
     (sym symbol?)
     (type type?)
     (tenv type-environment?)))
  
  (define empty-tenv empty-tenv-record)
  (define extend-tenv extended-tenv-record)
  
  (define apply-tenv 
    (lambda (tenv sym)
      (cases type-environment tenv
        (empty-tenv-record ()
                           (eopl:error 'apply-tenv "Unbound variable ~s" sym))
        (extended-tenv-record (sym1 val1 old-env)
                              (if (eqv? sym sym1)
                                  val1
                                  (apply-tenv old-env sym))))))
  
  (define init-tenv
    (lambda ()
      (extend-tenv 'x (int-type) 
                   (extend-tenv 'v (int-type)
                                (extend-tenv 'i (int-type)
                                             (empty-tenv))))))
  
  (define fresh-tvar-type
    (let ((sn 0))
      (lambda ()
        (set! sn (+ sn 1))
        (tvar-type sn))))
  
  (define otype->type
    (lambda (otype)
      (cases optional-type otype
        (no-type () (fresh-tvar-type))
        (a-type (ty) ty))))
  )